Erasure-Lambda.agda:7,29-30
Variable y is declared erased, so it cannot be used here
when checking that the expression y has type _B_7
